H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.76 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Monad

((liftM3 :: (b -> a -> c -> d) -> [b] -> [a] -> [c] -> [d]) :: (b -> a -> c -> d) -> [b] -> [a] -> [c] -> [d])

module Monad where

import qualified Maybe
import qualified Prelude

liftM3 :: Monad c => (a -> d -> b -> e) -> c a -> c d -> c b -> c e

liftM3

f m1 m2 m3

m1 >>= (\x1 ->m2 >>= (\x2 ->m3 >>= (\x3 ->return (f x1 x2 x3))))

module Maybe where

import qualified Monad
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\x3→return (f x1 x2 x3)

is transformed to

liftM30 f x1 x2 x3 = return (f x1 x2 x3)

The following Lambda expression

\x2→m3 >>= liftM30 f x1 x2

is transformed to

liftM31 m3 f x1 x2 = m3 >>= liftM30 f x1 x2

The following Lambda expression

\x1→m2 >>= liftM31 m3 f x1

is transformed to

liftM32 m2 m3 f x1 = m2 >>= liftM31 m3 f x1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Monad

((liftM3 :: (d -> b -> a -> c) -> [d] -> [b] -> [a] -> [c]) :: (d -> b -> a -> c) -> [d] -> [b] -> [a] -> [c])

module Maybe where

import qualified Monad
import qualified Prelude

module Monad where

import qualified Maybe
import qualified Prelude

liftM3 :: Monad e => (c -> a -> b -> d) -> e c -> e a -> e b -> e d

liftM3

f m1 m2 m3

m1 >>= liftM32 m2 m3 f

liftM30

f x1 x2 x3

return (f x1 x2 x3)

liftM31

m3 f x1 x2

m3 >>= liftM30 f x1 x2

liftM32

m2 m3 f x1

m2 >>= liftM31 m3 f x1

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Monad

((liftM3 :: (b -> a -> d -> c) -> [b] -> [a] -> [d] -> [c]) :: (b -> a -> d -> c) -> [b] -> [a] -> [d] -> [c])

module Monad where

import qualified Maybe
import qualified Prelude

liftM3 :: Monad c => (d -> a -> e -> b) -> c d -> c a -> c e -> c b

liftM3

f m1 m2 m3

m1 >>= liftM32 m2 m3 f

liftM30

f x1 x2 x3

return (f x1 x2 x3)

liftM31

m3 f x1 x2

m3 >>= liftM30 f x1 x2

liftM32

m2 m3 f x1

m2 >>= liftM31 m3 f x1

module Maybe where

import qualified Monad
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule Monad

(liftM3 :: (a -> d -> b -> c) -> [a] -> [d] -> [b] -> [c])

module Maybe where

import qualified Monad
import qualified Prelude

module Monad where

import qualified Maybe
import qualified Prelude

liftM3 :: Monad d => (c -> e -> b -> a) -> d c -> d e -> d b -> d a

liftM3

f m1 m2 m3

m1 >>= liftM32 m2 m3 f

liftM30

f x1 x2 x3

return (f x1 x2 x3)

liftM31

m3 f x1 x2

m3 >>= liftM30 f x1 x2

liftM32

m2 m3 f x1

m2 >>= liftM31 m3 f x1

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="liftM3",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="liftM3 vy3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="liftM3 vy3 vy4",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="liftM3 vy3 vy4 vy5",fontsize=16,color="grey",shape="box"];5 -> 6[label="",style="dashed", color="grey", weight=3];
6[label="liftM3 vy3 vy4 vy5 vy6",fontsize=16,color="black",shape="triangle"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="vy4 >>= liftM32 vy5 vy6 vy3",fontsize=16,color="burlywood",shape="triangle"];67[label="vy4/vy40 : vy41",fontsize=10,color="white",style="solid",shape="box"];7 -> 67[label="",style="solid", color="burlywood", weight=9];
67 -> 8[label="",style="solid", color="burlywood", weight=3];
68[label="vy4/[]",fontsize=10,color="white",style="solid",shape="box"];7 -> 68[label="",style="solid", color="burlywood", weight=9];
68 -> 9[label="",style="solid", color="burlywood", weight=3];
8[label="vy40 : vy41 >>= liftM32 vy5 vy6 vy3",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="[] >>= liftM32 vy5 vy6 vy3",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10 -> 27[label="",style="dashed", color="red", weight=0];
10[label="liftM32 vy5 vy6 vy3 vy40 ++ (vy41 >>= liftM32 vy5 vy6 vy3)",fontsize=16,color="magenta"];10 -> 28[label="",style="dashed", color="magenta", weight=3];
10 -> 29[label="",style="dashed", color="magenta", weight=3];
11[label="[]",fontsize=16,color="green",shape="box"];28 -> 7[label="",style="dashed", color="red", weight=0];
28[label="vy41 >>= liftM32 vy5 vy6 vy3",fontsize=16,color="magenta"];28 -> 38[label="",style="dashed", color="magenta", weight=3];
29[label="liftM32 vy5 vy6 vy3 vy40",fontsize=16,color="black",shape="box"];29 -> 39[label="",style="solid", color="black", weight=3];
27[label="vy8 ++ vy7",fontsize=16,color="burlywood",shape="triangle"];71[label="vy8/vy80 : vy81",fontsize=10,color="white",style="solid",shape="box"];27 -> 71[label="",style="solid", color="burlywood", weight=9];
71 -> 40[label="",style="solid", color="burlywood", weight=3];
72[label="vy8/[]",fontsize=10,color="white",style="solid",shape="box"];27 -> 72[label="",style="solid", color="burlywood", weight=9];
72 -> 41[label="",style="solid", color="burlywood", weight=3];
38[label="vy41",fontsize=16,color="green",shape="box"];39[label="vy5 >>= liftM31 vy6 vy3 vy40",fontsize=16,color="burlywood",shape="triangle"];73[label="vy5/vy50 : vy51",fontsize=10,color="white",style="solid",shape="box"];39 -> 73[label="",style="solid", color="burlywood", weight=9];
73 -> 42[label="",style="solid", color="burlywood", weight=3];
74[label="vy5/[]",fontsize=10,color="white",style="solid",shape="box"];39 -> 74[label="",style="solid", color="burlywood", weight=9];
74 -> 43[label="",style="solid", color="burlywood", weight=3];
40[label="(vy80 : vy81) ++ vy7",fontsize=16,color="black",shape="box"];40 -> 44[label="",style="solid", color="black", weight=3];
41[label="[] ++ vy7",fontsize=16,color="black",shape="box"];41 -> 45[label="",style="solid", color="black", weight=3];
42[label="vy50 : vy51 >>= liftM31 vy6 vy3 vy40",fontsize=16,color="black",shape="box"];42 -> 46[label="",style="solid", color="black", weight=3];
43[label="[] >>= liftM31 vy6 vy3 vy40",fontsize=16,color="black",shape="box"];43 -> 47[label="",style="solid", color="black", weight=3];
44[label="vy80 : vy81 ++ vy7",fontsize=16,color="green",shape="box"];44 -> 48[label="",style="dashed", color="green", weight=3];
45[label="vy7",fontsize=16,color="green",shape="box"];46 -> 27[label="",style="dashed", color="red", weight=0];
46[label="liftM31 vy6 vy3 vy40 vy50 ++ (vy51 >>= liftM31 vy6 vy3 vy40)",fontsize=16,color="magenta"];46 -> 49[label="",style="dashed", color="magenta", weight=3];
46 -> 50[label="",style="dashed", color="magenta", weight=3];
47[label="[]",fontsize=16,color="green",shape="box"];48 -> 27[label="",style="dashed", color="red", weight=0];
48[label="vy81 ++ vy7",fontsize=16,color="magenta"];48 -> 51[label="",style="dashed", color="magenta", weight=3];
49 -> 39[label="",style="dashed", color="red", weight=0];
49[label="vy51 >>= liftM31 vy6 vy3 vy40",fontsize=16,color="magenta"];49 -> 52[label="",style="dashed", color="magenta", weight=3];
50[label="liftM31 vy6 vy3 vy40 vy50",fontsize=16,color="black",shape="box"];50 -> 53[label="",style="solid", color="black", weight=3];
51[label="vy81",fontsize=16,color="green",shape="box"];52[label="vy51",fontsize=16,color="green",shape="box"];53[label="vy6 >>= liftM30 vy3 vy40 vy50",fontsize=16,color="burlywood",shape="triangle"];78[label="vy6/vy60 : vy61",fontsize=10,color="white",style="solid",shape="box"];53 -> 78[label="",style="solid", color="burlywood", weight=9];
78 -> 54[label="",style="solid", color="burlywood", weight=3];
79[label="vy6/[]",fontsize=10,color="white",style="solid",shape="box"];53 -> 79[label="",style="solid", color="burlywood", weight=9];
79 -> 55[label="",style="solid", color="burlywood", weight=3];
54[label="vy60 : vy61 >>= liftM30 vy3 vy40 vy50",fontsize=16,color="black",shape="box"];54 -> 56[label="",style="solid", color="black", weight=3];
55[label="[] >>= liftM30 vy3 vy40 vy50",fontsize=16,color="black",shape="box"];55 -> 57[label="",style="solid", color="black", weight=3];
56 -> 27[label="",style="dashed", color="red", weight=0];
56[label="liftM30 vy3 vy40 vy50 vy60 ++ (vy61 >>= liftM30 vy3 vy40 vy50)",fontsize=16,color="magenta"];56 -> 58[label="",style="dashed", color="magenta", weight=3];
56 -> 59[label="",style="dashed", color="magenta", weight=3];
57[label="[]",fontsize=16,color="green",shape="box"];58 -> 53[label="",style="dashed", color="red", weight=0];
58[label="vy61 >>= liftM30 vy3 vy40 vy50",fontsize=16,color="magenta"];58 -> 60[label="",style="dashed", color="magenta", weight=3];
59[label="liftM30 vy3 vy40 vy50 vy60",fontsize=16,color="black",shape="box"];59 -> 61[label="",style="solid", color="black", weight=3];
60[label="vy61",fontsize=16,color="green",shape="box"];61[label="return (vy3 vy40 vy50 vy60)",fontsize=16,color="black",shape="box"];61 -> 62[label="",style="solid", color="black", weight=3];
62[label="vy3 vy40 vy50 vy60 : []",fontsize=16,color="green",shape="box"];62 -> 63[label="",style="dashed", color="green", weight=3];
63[label="vy3 vy40 vy50 vy60",fontsize=16,color="green",shape="box"];63 -> 64[label="",style="dashed", color="green", weight=3];
63 -> 65[label="",style="dashed", color="green", weight=3];
63 -> 66[label="",style="dashed", color="green", weight=3];
64[label="vy40",fontsize=16,color="green",shape="box"];65[label="vy50",fontsize=16,color="green",shape="box"];66[label="vy60",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(vy80, vy81), vy7, h) → new_psPs(vy81, vy7, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_psPs(:(vy80, vy81), vy7, h) → new_psPs(vy81, vy7, h)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs(:(vy60, vy61), vy3, vy40, vy50, h, ba, bb, bc) → new_gtGtEs(vy61, vy3, vy40, vy50, h, ba, bb, bc)

From the DPs we obtained the following set of size-change graphs:

new_gtGtEs(:(vy60, vy61), vy3, vy40, vy50, h, ba, bb, bc) → new_gtGtEs(vy61, vy3, vy40, vy50, h, ba, bb, bc)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 8 >= 8

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs0(:(vy50, vy51), vy6, vy3, vy40, h, ba, bb, bc) → new_gtGtEs0(vy51, vy6, vy3, vy40, h, ba, bb, bc)

From the DPs we obtained the following set of size-change graphs:

new_gtGtEs0(:(vy50, vy51), vy6, vy3, vy40, h, ba, bb, bc) → new_gtGtEs0(vy51, vy6, vy3, vy40, h, ba, bb, bc)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 8 >= 8

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs1(:(vy40, vy41), vy5, vy6, vy3, h, ba, bb, bc) → new_gtGtEs1(vy41, vy5, vy6, vy3, h, ba, bb, bc)

From the DPs we obtained the following set of size-change graphs:

new_gtGtEs1(:(vy40, vy41), vy5, vy6, vy3, h, ba, bb, bc) → new_gtGtEs1(vy41, vy5, vy6, vy3, h, ba, bb, bc)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 8 >= 8